Nuprl Definition : LocKnd
11,40
postcript
pdf
LocKnd == {
ik
:
:Id
Knd| let
i
,
k
=
ik
in
hasloc(
k
;
i
)}
latex
Definitions
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
Id
,
Knd
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
b
,
hasloc(
k
;
i
)
FDL editor aliases
LocKnd
origin
Knd| let i,k = ik in 
hasloc(k; i)} Knd| let i,k = ik in hasloc(k; i)} B(x)b